Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		not(x)	→ if(x,false,true)
2:		and(x,y)	→ if(x,y,false)
3:		or(x,y)	→ if(x,true,y)
4:		implies(x,y)	→ if(x,y,true)
5:		x = x	→ true
6:		x = y	→ if(x,y,not(y))
7:		if(true,x,y)	→ x
8:		if(false,x,y)	→ y
9:		if(x,x,if(x,false,true))	→ true
10:		x = y	→ if(x,y,if(y,false,true))

There are 8 dependency pairs:


11:		NOT(x)	→ IF(x,false,true)
12:		AND(x,y)	→ IF(x,y,false)
13:		OR(x,y)	→ IF(x,true,y)
14:		IMPLIES(x,y)	→ IF(x,y,true)
15:		x =# y	→ IF(x,y,not(y))
16:		x =# y	→ NOT(y)
17:		x =# y	→ IF(x,y,if(y,false,true))
18:		x =# y	→ IF(y,false,true)

The approximated dependency graph contains no SCCs and hence the TRS is trivially terminating.

Tyrolean Termination Tool (0.01 seconds) --- May 4, 2006